Nuprl Lemma : ma-single-sframe_wf
0,22
postcript
pdf
l
:IdLnk,
tg
:Id,
L
:Knd List. only
L
sends on (
l
with
tg
)
MsgA
latex
Definitions
t
T
,
x
.
t
(
x
)
,
x
:
A
.
B
(
x
)
,
,
Prop
,
only
L
sends on (
l
with
tg
)
Lemmas
mk-ma
wf
,
ma-state
wf
,
top
wf
,
fpf-single
wf
,
IdLnk
wf
,
fpf-empty
wf
,
Knd
wf
,
Id
wf
origin
l:IdLnk, tg:Id, L:Knd List. only L sends on (l with tg) 
MsgA l:IdLnk, tg:Id, L:Knd List. only L sends on (l with tg) MsgA T
x. t(x)x:A. B(x)